\begin{tabbing}
(\=UnivCD THENA Auto) \+
\\[0ex]CollapseTHEN ((RepUR ``mu$\backslash$' can{-}apply`` ( 0)$\cdot$) 
\\[0ex]CollapseTHEN ((
\-\\[0ex]S\=ubst' TERMOF\{p{-}mu{-}decider:ObjectId, 1:l, 1:l\} $\sim$ TERMOF\{p{-}mu{-}decider:ObjectId, 1:l, i:l\}\+
\\[0ex]( 0)$\cdot$) 
\\[0ex]THENL [(RW (SubC (ComputeToC []) ) 0) 
\\[0ex]CollapseTHEN (Trivial)$\cdot$ ; Id]$\cdot$)$\cdot$)$\cdot$
\-
\end{tabbing}